Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Ja, herzlich willkommen. Ja, heute machen wir mal was Richtiges und zwar...

Zwar werden wir zeigen die Vollständigkeit des Resolutionsalgorithmus, den wir am Ende der

letzten Sitzung kennengelernt haben und zu diesen Berufe werden wir vorher ein Theoriegebäude hochziehen,

das nennt sich A-Brand Theorie. Das heißt, wir werden kennenlernen eine Modellkonstruktion für

Logik erster Stufe. Da wird aus dieser Modellkonstruktion etliches an sehr unmittelbaren

Konsequenzen rausfallen. Das ist zum einen die Halbentscheidbarkeit der Logik, das ist zweitens

die Kompaktheit der Logik und das ist drittens der berühmte Satz von Löwenheims Golem. Jede First

Order Theorie hat abzählbare Modelle. Wie erstaunlich der ist, das diskutieren wir dann, wenn er dransteht.

So, Disclaimer vorneweg, man kann das auch mit Gleichheit machen, dann wird die Konstruktion

der Modelle einschlagkomplizierter, dann muss ich sie nochmal quotientieren, dann muss man über

Quotienten von Mengen von Modulo-Äquivalenzrelationen reden, das macht erfahrungsgemäß Schwierigkeiten,

also lasse ich es jetzt mal weg. Also wir vereinfachen die Logik zu der Logik ohne

Gleichheit, das ist im Grunde nicht schlimm, denn man kann ja Gleichheit emulieren gewissermaßen,

indem man einfach ein binäres Prädikat einführt und sagt, das ist halt reflexiv und symmetrisch

und transitiv und das nennen wir jetzt Gleichheit und alle Operationen sind Konkurrenzen bezüglich

dieser Gleichheit und alle Prädikate sind abgeschlossen darunter, dann hat man seine

Gleichheit. Das stört also eigentlich nicht weiter.

So, und wir definieren einfach gleich mal vorweg die Trägermenge unserer Universen,

also ohne Einschränkung fehlt noch. Ohne Einschränkung enthalte unsere Signatur mal eine Konstante.

So, es gibt natürlich Signaturen, die tun das nicht, dann fügen wir halt einfach irgendeine

Dummi-Konstante hinzu. Der Grund, dass das tatsächlich ohne Einschränkung ist, ist der,

dass wir gesagt haben, dass die Modelle nicht leer sind. Also die Modelle, ich kann praktisch

jedes Modell, was noch keine Konstante hat, kann ich um eine Konstante erweitern, indem

ich dieses Symbol einfach irgendwie interpretiere. Das würde natürlich nicht gehen, wenn das

leere Modell zugelassen wäre, indem könnte ich nämlich eine Konstante nicht interpretieren,

weil ich ja keinen Wert finde, den ich ihr zuweisen kann. So, das ist hier aber nicht

so. Das heißt also ohne Einschränkung gibt es eine Konstante.

So, und zwar ist die Trägermenge aller diese Erbraunmodelle dann das sogenannte Erbraun-Universum.

Das schreiben wir U-Sigma, um anzudeuten, dass es natürlich von der Signatur, mit der wir

da reingehen, abhängt. Und zwar

ist das die Menge aller sogenannten Grundtherme, natürlich über Sigma, so schreibe ich jetzt

nicht noch mit in die Notation rein. Und was heißt Grundtherme? Nun Grundtherme heißt

einfach, dass der Therm keine Variablen enthält. Das sind also alle Terme E, natürlich Sigma-Therme,

die in der Variablenmenge leer sind. So, das darf ich deswegen später als Trägermenge

eines Modells verwenden, weil ich diese Annahme hier gemacht habe. Wenn es nämlich keine Konstante

gibt, dann gibt es auch keine Terme ohne Variablen. Da kriege ich einfach keinen Term

hingeschrieben. Und dann wäre das Erbraun-Universum leer und käme insofern also nicht als Trägermenge

eines Modells in Frage. So, das war der Grund für diese Annahme.

So, dann vereinfachen wir für solche Terme noch ein bisschen die Schreibweise, weil die

nämlich keine Variablen enthalten, hängen sie natürlich auch von den Werten der Variablen

nicht ab. Das heißt, wenn wir so einen Term E in einem Modell auswerten unter einer Umgebung

Eta, dann hängt das von dieser Umgebung Eta nicht ab. Das heißt, wir können einfach

schreiben M von E, lassen die Umgebung also weg. Ja, machen wir mal ein Beispiel, nehmen

wir uns also eine Signatur her. Haben wir schon mal gesehen, das ist die für die natürlichen

Zahlen mit diesem Ungratheitspredikat. Das heißt, die hat eine einstellige Successor-Funktion,

die hat eine konstante Z wie 0 und sie hat so ein einstelliges Ungratheitspredikat,

groß u wie odd. Und dann haben wir folgendes Erbraun-Universum. Na ja, das sind eben alle

Terme, die ich ohne Variablen hinschreiben kann. Da haben wir uns schon überlegt, was

das ist. Das ist einmal Z kann ich hinschreiben, weil es eine Konstante ist, dann S von Z und